feat: enable backward.isDefEq.respectTransparency.types by default by datokrat · Pull Request #13895 · leanprover/lean4

datokrat · 2026-05-29T19:06:42Z

No description provided.

mathlib-lean-pr-testing · 2026-05-29T19:18:40Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-13895 build this PR didn't complete normally. (2026-05-29 19:18:38) View Log
✅ Mathlib branch lean-pr-testing-13895 has successfully built against this PR. (2026-05-29 21:09:04) View Log
✅ Mathlib branch lean-pr-testing-13895 has successfully built against this PR. (2026-06-02 09:35:44) View Log
✅ Mathlib branch lean-pr-testing-13895 has successfully built against this PR. (2026-06-02 11:50:19) View Log

leanprover-bot · 2026-05-29T20:15:46Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-29 20:15:45)

datokrat · 2026-06-01T18:33:10Z

!radar

leanprover-radar · 2026-06-01T18:33:17Z

Benchmark results for bc527c4 against d9ee0ed are in. There are significant results. @datokrat

🟥 build//instructions: +208.0G (+1.84%)

Large changes (1✅, 15🟥)

🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +12.2G (+6.39%)
🟥 build/module/Std.Data.DTreeMap.Lemmas//instructions: +5.3G (+9.29%)
🟥 build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: +5.1G (+7.49%)
✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: -5.3G (-32.57%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: +7.8G (+19.42%)
🟥 compiled/hashmap//instructions: +1.2G (+36.43%)
🟥 compiled/hashmap//task-clock: +47ms (+26.80%)
🟥 compiled/hashmap//wall-clock: +46ms (+26.70%)
🟥 compiled/liasolver//instructions: +151.5M (+3.79%)
🟥 compiled/parser//instructions: +269.1M (+0.78%)
🟥 compiled/qsort//task-clock: +376ms (+32.09%)
🟥 compiled/qsort//wall-clock: +376ms (+32.09%)
🟥 elab/big_do//instructions: +218.8M (+1.01%)
🟥 elab/big_match_nat_split//instructions: +443.5M (+4.12%)
🟥 elab/big_omega//instructions: +1.1G (+4.97%)
🟥 elab/big_omega_MT//instructions: +1.1G (+5.24%)

Medium changes (1✅, 50🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (16✅, 1200🟥)

Too many entries to display here. View the full report on radar instead.

leanprover-radar · 2026-06-02T07:55:12Z

Benchmark results for bdc3f56 against d9ee0ed are in. There are significant results. @implausibility

🟥 build//instructions: +11.0G (+0.10%)

Large changes (1✅, 2🟥)

✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: -5.5G (-33.69%)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: +7.1G (+17.82%)
🟥 compiled/parser//instructions: +268.7M (+0.78%)

Medium changes (1✅, 5🟥)

🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Clause//instructions: +1.4G (+26.07%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas//instructions: +2.1G (+13.64%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult//instructions: +2.1G (+20.02%) (reduced significance based on absolute threshold)
🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound//instructions: +1.1G (+8.22%) (reduced significance based on absolute threshold)
🟥 build/profile/grind//wall-clock: +2s (+45.01%)
✅ elab/cbv_decide//instructions: -573.8M (-1.31%)

Small changes (28✅, 36🟥)

Too many entries to display here. View the full report on radar instead.

datokrat · 2026-06-02T10:02:48Z

!radar

leanprover-radar · 2026-06-02T10:02:54Z

Benchmark results for d5f7bfb against d9ee0ed are in. There are significant results. @datokrat

✅ build//instructions: -5.3G (-0.05%)

Large changes (1✅, 1🟥)

✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: -5.5G (-33.69%)
🟥 compiled/parser//instructions: +269.3M (+0.78%)

Medium changes (1✅)

✅ elab/cbv_decide//instructions: -580.6M (-1.32%)

Small changes (30✅, 35🟥)

Too many entries to display here. View the full report on radar instead.

This PR refines the "One might expect/hope" annotations so each one states precisely where the failure surfaces: the stage 2 build, or a specific test (noting that the `binderNameHint` test failure only appears in a stage 2 build). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…tions This PR adds `implicit_reducible` and/or `expose` attributes to definitions that need to be unfolded during defeq checking without full transparency. Preparatory commit for removing the TODO workaround in ExprDefEq.lean. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

(#13584) This PR fixes some warnings in stage2 due to redundant `@[expose]`.

This reverts commit cc007d9.

…for now" This reverts commit 987c895.

This reverts commit d74fd4a.

snapshot (failing) snapshot (succeeding, Init.Prelude still having too many instance_reducible attributes) done

datokrat added the force-mathlib-ci label May 29, 2026

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 29, 2026

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label May 29, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 29, 2026

Update lean-toolchain for leanprover/lean4#13895

8fcbe41

mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 29, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jun 2, 2026

Update lean-toolchain for leanprover/lean4#13895

8f61db6

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 2, 2026

Update lean-toolchain for leanprover/lean4#13895

b6ef27d

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jun 2, 2026

Update lean-toolchain for leanprover/lean4#13895

a483525

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 2, 2026

Update lean-toolchain for leanprover/lean4#13895

19fb046

kim-em and others added 14 commits June 2, 2026 13:43

perf: do specialize implicit-reducible declarations

0b3ad46

chore: update stage0

8b91b34

test: update tests for defeq changes

85812e1

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

chore: add implicit_reducible/expose attributes to library definitions

9fdf3c0

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

feat: enable backward.isDefEq.respectTransparency.types by default

de2c3ec

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: update tests for defeq changes

2796eeb

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

fix: add Option.map_some to modify_eq_alter simp sets

0866b72

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

fix: remove @[expose] when unnecessary, fixing stage2 warnings in #13823

8b10292

(#13584) This PR fixes some warnings in stage2 due to redundant `@[expose]`.

fix errors from rebasing

2568241

remove respectTransparency.types false

8ce9dfe

remove local attributes

258b8e8

cleanup

bb88d6a

datokrat added 16 commits June 2, 2026 13:58

dsimproc test

d80e6da

snapshot

0735ff8

Revert "snapshot"

a579504

This reverts commit cc007d9.

remove test files; I gave up trying to satisfy the dsimprocs for now

f7dde73

Revert "remove test files; I gave up trying to satisfy the dsimprocs …

9c2b24d

…for now" This reverts commit 987c895.

implicit -> instance

451684e

Reapply "snapshot"

4eff7b1

This reverts commit d74fd4a.

poke

90b2fbb

it compiles

78cf1b9

linter

c981ea3

make Not implicit_reducible

1108e16

less instance_reducible

6554255

snapshot (failing) snapshot (succeeding, Init.Prelude still having too many instance_reducible attributes) done

shiftLeft/shiftRight implicit_reducible

5e21cb9

rebasing fixes

431ee6e

more implicit_reducible, fixing mathlib linter errors

696acf1

make PosFin only implicit-reducible

89bf42e

datokrat force-pushed the defeq_todo_4_paul_nwm branch from d5f7bfb to 89bf42e Compare June 2, 2026 12:03

datokrat changed the title ~~fix: respectTransparency (new mathlib)~~ feat: enable backward.isDefEq.respectTransparency.types by default Jun 2, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: enable backward.isDefEq.respectTransparency.types by default#13895

feat: enable backward.isDefEq.respectTransparency.types by default#13895
datokrat wants to merge 30 commits into
paul/base/defeq_todo_4_paul_nwmfrom
defeq_todo_4_paul_nwm

datokrat commented May 29, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented May 29, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented May 29, 2026

Uh oh!

datokrat commented Jun 1, 2026

Uh oh!

leanprover-radar commented Jun 1, 2026 •

edited

Loading

Uh oh!

leanprover-radar commented Jun 2, 2026 •

edited

Loading

Uh oh!

datokrat commented Jun 2, 2026

Uh oh!

leanprover-radar commented Jun 2, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

datokrat commented May 29, 2026

Uh oh!

mathlib-lean-pr-testing Bot commented May 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented May 29, 2026

Uh oh!

datokrat commented Jun 1, 2026

Uh oh!

leanprover-radar commented Jun 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-radar commented Jun 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

datokrat commented Jun 2, 2026

Uh oh!

leanprover-radar commented Jun 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

mathlib-lean-pr-testing Bot commented May 29, 2026 •

edited

Loading

leanprover-radar commented Jun 1, 2026 •

edited

Loading

leanprover-radar commented Jun 2, 2026 •

edited

Loading

leanprover-radar commented Jun 2, 2026 •

edited

Loading